package edu.arizona.bio5.onto.decomposition.locality;

import java.util.Collection;

import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLClassExpression;
import org.semanticweb.owlapi.model.OWLClassExpressionVisitor;
import org.semanticweb.owlapi.model.OWLDataAllValuesFrom;
import org.semanticweb.owlapi.model.OWLDataExactCardinality;
import org.semanticweb.owlapi.model.OWLDataHasValue;
import org.semanticweb.owlapi.model.OWLDataMaxCardinality;
import org.semanticweb.owlapi.model.OWLDataMinCardinality;
import org.semanticweb.owlapi.model.OWLDataSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLEntity;
import org.semanticweb.owlapi.model.OWLObjectAllValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectComplementOf;
import org.semanticweb.owlapi.model.OWLObjectExactCardinality;
import org.semanticweb.owlapi.model.OWLObjectHasSelf;
import org.semanticweb.owlapi.model.OWLObjectHasValue;
import org.semanticweb.owlapi.model.OWLObjectIntersectionOf;
import org.semanticweb.owlapi.model.OWLObjectMaxCardinality;
import org.semanticweb.owlapi.model.OWLObjectMinCardinality;
import org.semanticweb.owlapi.model.OWLObjectOneOf;
import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectUnionOf;
import com.clarkparsia.owlapi.modularity.locality.LocalityClass;


/**
 * Used to determine if class expressions are equivalent to \bottom using the provided locality class
 */
public class BottomEquivalenceEvaluator implements OWLClassExpressionVisitor {

    private boolean isBottomEquivalent;

    private LocalityClass localityCls;

    private Collection<? extends OWLEntity> signature;

    private TopEquivalenceEvaluator topEvaluator = null;


    public BottomEquivalenceEvaluator() {
    }


    private boolean isBottomEquivalent(OWLClassExpression desc) {
        desc.accept(this);
        return isBottomEquivalent;
    }


    public boolean isBottomEquivalent(OWLClassExpression desc, Collection<? extends OWLEntity> signature, LocalityClass localityCls) {
        this.localityCls = localityCls;
        this.signature = signature;
        desc.accept(this);
        return isBottomEquivalent;
    }


    public void setTopEvaluator(TopEquivalenceEvaluator evaluator) {
        this.topEvaluator = evaluator;
    }


    public void visit(OWLClass desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
                isBottomEquivalent = desc.isOWLNothing() || (!desc.isOWLThing() && !signature.contains(desc));
                break;
            case TOP_BOTTOM:
            case TOP_TOP:
                isBottomEquivalent = desc.isOWLNothing();
                break;
        }
    }


    // BUGFIX: (TS) Even in the TOP_TOP case, this is not bottom-equiv:
    //              "forall top.D" is not necessarily empty
    // BUGFIX: (TS, 3): In the TOP_TOP case, there is a bottom-equiv possibility.

    public void visit(OWLDataAllValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = false;
                break;
            case TOP_TOP:
                isBottomEquivalent = (!signature.contains(desc.getProperty().asOWLDataProperty()) && !desc.getFiller().isTopDatatype());
                break;
        }
    }


    // BUGFIX: (TS) Corrected both conditions; included case n==0
    // BUGFIX: (TS, 2) Added the cases where the filler is top-equiv
    // BUGFIX: (TS, 3) Repaired the cases where the filler is top-equiv

    public void visit(OWLDataExactCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = (desc.getCardinality() > 0) && (!signature.contains(desc.getProperty().asOWLDataProperty()));
                break;
            case TOP_TOP:
                isBottomEquivalent = 
                	(
                			(
                					(desc.getCardinality() == 0)
                					&& (
                							(!signature.contains(desc.getProperty().asOWLDataProperty())
                						)
                					&& LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))
                			)
                			||
                			(
                					(desc.getCardinality() > 0)
                					&& (
                							(!signature.contains(desc.getProperty().asOWLDataProperty())
                						)
                					&& LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller())
                					)
                			)
                	);
                break;
        }
    }


    // BUGFIX: (TS) A data max card restriction is never bottom-equiv.
    // BUGFIX: (TS, 2) Added the cases where the filler is top-equiv
    // BUGFIX: (TS, 3) Repaired the cases where the filler is top-equiv

    public void visit(OWLDataMaxCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = false;
                break;
            case TOP_TOP:
                isBottomEquivalent = (((desc.getCardinality() == 0) && ((!signature.contains(desc.getProperty().asOWLDataProperty())) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))) || ((desc.getCardinality() == 1) && ((!signature.contains(desc.getProperty().asOWLDataProperty())) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))) || ((desc.getCardinality() > 1) && ((!signature.contains(desc.getProperty().asOWLDataProperty())) && LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller()))));
                break;
        }
    }


    // BUGFIX: (TS) The *_BOTTOM case only works if n > 0.

    public void visit(OWLDataMinCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = (desc.getCardinality() > 0) && (!signature.contains(desc.getProperty().asOWLDataProperty()));
                break;
            case TOP_TOP:
                isBottomEquivalent = false;
                break;
        }
    }


    public void visit(OWLDataSomeValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = !signature.contains(desc.getProperty().asOWLDataProperty());
                break;
            case TOP_TOP:
                isBottomEquivalent = false;
                break;
        }
    }


    public void visit(OWLDataHasValue desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = !signature.contains(desc.getProperty().asOWLDataProperty());
                break;
            case TOP_TOP:
                isBottomEquivalent = false;
                break;
        }
    }


    // BUGFIX (TS): TOP_TOP case was missing the first conjunct

    public void visit(OWLObjectAllValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = false;
                break;
            case TOP_TOP:
                isBottomEquivalent = !signature.contains(desc.getProperty().getNamedProperty()) && isBottomEquivalent(desc.getFiller());
                break;
        }
    }


    public void visit(OWLObjectComplementOf desc) {
        isBottomEquivalent = topEvaluator.isTopEquivalent(desc.getOperand(), signature, localityCls);
    }


    // BUGFIX: (TS) Since an exact card restriction is a conjunction of a min and a max card restriction,
    //              there are cases where it is bottom-local

    public void visit(OWLObjectExactCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = (desc.getCardinality() > 0) && (!signature.contains(desc.getProperty().getNamedProperty()) || isBottomEquivalent(desc.getFiller()));
                break;
            case TOP_TOP:
                isBottomEquivalent = ((desc.getCardinality() > 0) && (isBottomEquivalent(desc.getFiller()) || ((!signature.contains(desc.getProperty().getNamedProperty())) && topEvaluator.isTopEquivalent(desc.getFiller(), signature, localityCls))));
                break;
        }
    }


    public void visit(OWLObjectIntersectionOf desc) {
        for (OWLClassExpression conj : desc.getOperands()) {
            if (isBottomEquivalent(conj)) {
                isBottomEquivalent = true;
                return;
            }
        }
        isBottomEquivalent = false;
    }


    // BUGFIX (TS): Corrected all conditions.
    //              The n==0 case doesn't affect bottom-equivalence of this type of restriction,
    //              but n>0 does!

    public void visit(OWLObjectMaxCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = false;
                break;
            case TOP_TOP:
                isBottomEquivalent = (desc.getCardinality() > 0) && (!signature.contains(desc.getProperty().getNamedProperty())) && topEvaluator.isTopEquivalent(desc.getFiller(), signature, localityCls);
                break;
        }
    }


    // BUGFIX (TS): Corrected all conditions, considering the case n==0

    public void visit(OWLObjectMinCardinality desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = (desc.getCardinality() > 0) && (!signature.contains(desc.getProperty().getNamedProperty()) || isBottomEquivalent(desc.getFiller()));
                break;
            case TOP_TOP:
                isBottomEquivalent = (desc.getCardinality() > 0) && isBottomEquivalent(desc.getFiller());
                break;
        }
    }


    public void visit(OWLObjectOneOf desc) {
        isBottomEquivalent = desc.getIndividuals().isEmpty();
    }


    public void visit(OWLObjectHasSelf desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = !signature.contains(desc.getProperty().getNamedProperty());
                break;
            case TOP_TOP:
                isBottomEquivalent = false;
                break;
        }
    }


    public void visit(OWLObjectSomeValuesFrom desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = !signature.contains(desc.getProperty().getNamedProperty()) || isBottomEquivalent(desc.getFiller());
                break;
            case TOP_TOP:
                isBottomEquivalent = isBottomEquivalent(desc.getFiller());
                break;
        }
    }


    public void visit(OWLObjectUnionOf desc) {
        for (OWLClassExpression disj : desc.getOperands()) {
            if (!isBottomEquivalent(disj)) {
                isBottomEquivalent = false;
                return;
            }
        }
        isBottomEquivalent = true;
    }


    // BUGFIX (TS): desc.getValue() is an individual and therefore is *not* bot-equiv if not in the signature
    //              -> disjunct removed from *_BOTTOM case

    public void visit(OWLObjectHasValue desc) {
        switch (localityCls) {
            case BOTTOM_BOTTOM:
            case TOP_BOTTOM:
                isBottomEquivalent = !signature.contains(desc.getProperty().getNamedProperty());
                break;
            case TOP_TOP:
                isBottomEquivalent = false;
                break;
        }
    }
}
